\begin{tabbing}
d{-}world($D$;$v$;${\it sched}$;${\it dec}$;${\it discrete}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<\lambda$$i$,$x$. M($i$).ds($x$)\+
\\[0ex], $\lambda$$i$,$a$. M($i$).da(locl($a$))
\\[0ex], $\lambda$$l$,${\it tg}$. M(source($l$)).dout($l$,${\it tg}$)
\\[0ex], $\lambda$$i$,$t$. if ($t$ =$_{0}$ 0)
\\[0ex]then $\lambda$$x$.M($i$).init($x$)?$v$($i$,$x$)
\\[0ex]else (CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))(($t$ {-} 1),$i$)).1
\\[0ex]fi 
\\[0ex], $\lambda$$i$,$t$. ((CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))($t$,$i$)).2).1
\\[0ex], $\lambda$$i$,$t$. (CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))($t$,$i$)).2.2
\\[0ex], $\lambda$$i$.d{-}machine($i$;M($i$);${\it dec}$($i$))
\\[0ex], ${\it discrete}$
\\[0ex], $\cdot>$
\-
\end{tabbing}